#include "FormulaData.cuh"
#include "../Preprocessing/UnaryClausesRemover.cuh"
#include "../Preprocessing/RepeatedLiteralsRemover.cuh"

FormulaData::FormulaData(int max_number_of_clauses, bool remove_unary) :
formula_dev(max_number_of_clauses), formula_host()
{
	this->clauses_capacity = max_number_of_clauses;
	this->number_of_clauses = 0;
	this->number_of_variables = 0;
	this->largest_clause_size = 0;
	this->status_after_preprocessing = UNDEF;
	this->remove_unary = remove_unary;
}

void FormulaData::add_clause(Lit* literals, int clause_size)
{
	assert(number_of_clauses < clauses_capacity);

	Clause c_host;
	Clause c;

	create_clause_host(clause_size, c_host);

	for(int i = 0; i < clause_size; i++)
	{
		addLitToHost(literals[i], c_host);
	}

	if(clause_size > largest_clause_size)
	{
		largest_clause_size = clause_size;
	}

	formula_host.push_back(c_host);
	number_of_clauses++;

}

void FormulaData::set_number_of_variables(int n_of_variables)
{
	this->number_of_variables = n_of_variables;
}

void FormulaData::set_most_common_variable(Var variable, int frequency)
{
	this->most_common_variable = variable;
	this->frequency_of_most_common_variable = frequency;
}

Var FormulaData::get_most_common_variable()
{
	return most_common_variable;
}
int FormulaData::get_frequency_of_most_common_variable()
{
	return frequency_of_most_common_variable;
}

CUDAClauseVec FormulaData::get_formula_dev()
{
	return formula_dev;
}
vector< Clause > * FormulaData::get_formula_host()
{
	return &formula_host;
}

int FormulaData::get_number_of_clauses()
{
	return number_of_clauses;
}
int FormulaData::get_number_of_variables()
{
	return number_of_variables;
}

int FormulaData::get_largest_clause_size()
{
	return largest_clause_size;
}

void FormulaData::copy_host_clauses_to_dev()
{
	status_after_preprocessing = UNDEF;

	RepeatedLiteralsRemover rlr(formula_host, number_of_variables);
	rlr.process();
	status_after_preprocessing = rlr.get_status();

	if(remove_unary)
	{
		if(status_after_preprocessing == UNDEF)
		{
			UnaryClausesRemover ucr(&formula_host, number_of_variables);
			ucr.process();
			status_after_preprocessing = ucr.get_status();
			ucr.get_set_literals(set_literals);
		}
	}


	if(status_after_preprocessing == UNDEF)
		formula_dev.alloc_and_copy_to_dev(formula_host);

	number_of_clauses = formula_dev.size_of();

}

sat_status FormulaData::get_status_after_preprocessing()
{
	return status_after_preprocessing;
}

vector< Lit > * FormulaData::get_set_literals()
{
	return &set_literals;
}

__host__ void FormulaData::print_fomula()
{

	printf("Formula with %d clauses:", formula_host.size());
	for(std::vector<Clause>::iterator it = formula_host.begin(); it < formula_host.end(); ++it)
	{
		print_clause(*it);
		printf("\n");
	}

}
